YES 5.682 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule Main
  ((floor :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Lambda Reductions:
The following Lambda expression
\(_,r)→r

is transformed to
r0 (_,r) = r

The following Lambda expression
\(n,_)→n

is transformed to
n0 (n,_) = n

The following Lambda expression
\(_,r)→r

is transformed to
r1 (_,r) = r

The following Lambda expression
\(q,_)→q

is transformed to
q1 (q,_) = q



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule Main
  ((floor :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Case Reductions:
The following Case expression
case compare x y of
 EQ → o
 LT → LT
 GT → GT

is transformed to
primCompAux0 o EQ = o
primCompAux0 o LT = LT
primCompAux0 o GT = GT



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ IFR

mainModule Main
  ((floor :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



If Reductions:
The following If expression
if r < 0 then n - 1 else n

is transformed to
floor0 True = n - 1
floor0 False = n

The following If expression
if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to
primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0 x y False = Zero

The following If expression
if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to
primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)
primModNatS0 x y False = Succ x



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
HASKELL
              ↳ BR

mainModule Main
  ((floor :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
frac@(Double wy wz)

is replaced by the following term
Double wy wz

The bind variable of the following binding Pattern
frac@(Float xu xv)

is replaced by the following term
Float xu xv



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
HASKELL
                  ↳ COR

mainModule Main
  ((floor :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
compare x y
 | x == y
 = EQ
 | x <= y
 = LT
 | otherwise
 = GT

is transformed to
compare x y = compare3 x y

compare0 x y True = GT

compare1 x y True = LT
compare1 x y False = compare0 x y otherwise

compare2 x y True = EQ
compare2 x y False = compare1 x y (x <= y)

compare3 x y = compare2 x y (x == y)

The following Function with conditions
gcd' x 0 = x
gcd' x y = gcd' y (x `rem` y)

is transformed to
gcd' x vuz = gcd'2 x vuz
gcd' x y = gcd'0 x y

gcd'0 x y = gcd' y (x `rem` y)

gcd'1 True x vuz = x
gcd'1 vvu vvv vvw = gcd'0 vvv vvw

gcd'2 x vuz = gcd'1 (vuz == 0) x vuz
gcd'2 vvx vvy = gcd'0 vvx vvy

The following Function with conditions
gcd 0 0 = error []
gcd x y = 
gcd' (abs x) (abs y)
where 
gcd' x 0 = x
gcd' x y = gcd' y (x `rem` y)

is transformed to
gcd vvz vwu = gcd3 vvz vwu
gcd x y = gcd0 x y

gcd0 x y = 
gcd' (abs x) (abs y)
where 
gcd' x vuz = gcd'2 x vuz
gcd' x y = gcd'0 x y
gcd'0 x y = gcd' y (x `rem` y)
gcd'1 True x vuz = x
gcd'1 vvu vvv vvw = gcd'0 vvv vvw
gcd'2 x vuz = gcd'1 (vuz == 0) x vuz
gcd'2 vvx vvy = gcd'0 vvx vvy

gcd1 True vvz vwu = error []
gcd1 vwv vww vwx = gcd0 vww vwx

gcd2 True vvz vwu = gcd1 (vwu == 0) vvz vwu
gcd2 vwy vwz vxu = gcd0 vwz vxu

gcd3 vvz vwu = gcd2 (vvz == 0) vvz vwu
gcd3 vxv vxw = gcd0 vxv vxw

The following Function with conditions
reduce x y
 | y == 0
 = error []
 | otherwise
 = x `quot` d :% (y `quot` d)
where 
d  = gcd x y

is transformed to
reduce x y = reduce2 x y

reduce2 x y = 
reduce1 x y (y == 0)
where 
d  = gcd x y
reduce0 x y True = x `quot` d :% (y `quot` d)
reduce1 x y True = error []
reduce1 x y False = reduce0 x y otherwise

The following Function with conditions
absReal x
 | x >= 0
 = x
 | otherwise
 = `negate` x

is transformed to
absReal x = absReal2 x

absReal1 x True = x
absReal1 x False = absReal0 x otherwise

absReal0 x True = `negate` x

absReal2 x = absReal1 x (x >= 0)

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
HASKELL
                      ↳ LetRed

mainModule Main
  ((floor :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
floor0 (r < 0)
where 
floor0 True = n - 1
floor0 False = n
n  = n0 vu9
n0 (n,vw) = n
r  = r0 vu9
r0 (vv,r) = r
vu9  = properFraction x

are unpacked to the following functions on top level
floorN vxx = floorN0 vxx (floorVu9 vxx)

floorR0 vxx (vv,r) = r

floorVu9 vxx = properFraction vxx

floorR vxx = floorR0 vxx (floorVu9 vxx)

floorFloor0 vxx True = floorN vxx - 1
floorFloor0 vxx False = floorN vxx

floorN0 vxx (n,vw) = n

The bindings of the following Let/Where expression
reduce1 x y (y == 0)
where 
d  = gcd x y
reduce0 x y True = x `quot` d :% (y `quot` d)
reduce1 x y True = error []
reduce1 x y False = reduce0 x y otherwise

are unpacked to the following functions on top level
reduce2Reduce1 vxy vxz x y True = error []
reduce2Reduce1 vxy vxz x y False = reduce2Reduce0 vxy vxz x y otherwise

reduce2D vxy vxz = gcd vxy vxz

reduce2Reduce0 vxy vxz x y True = x `quot` reduce2D vxy vxz :% (y `quot` reduce2D vxy vxz)

The bindings of the following Let/Where expression
gcd' (abs x) (abs y)
where 
gcd' x vuz = gcd'2 x vuz
gcd' x y = gcd'0 x y
gcd'0 x y = gcd' y (x `rem` y)
gcd'1 True x vuz = x
gcd'1 vvu vvv vvw = gcd'0 vvv vvw
gcd'2 x vuz = gcd'1 (vuz == 0) x vuz
gcd'2 vvx vvy = gcd'0 vvx vvy

are unpacked to the following functions on top level
gcd0Gcd'0 x y = gcd0Gcd' y (x `rem` y)

gcd0Gcd'1 True x vuz = x
gcd0Gcd'1 vvu vvv vvw = gcd0Gcd'0 vvv vvw

gcd0Gcd'2 x vuz = gcd0Gcd'1 (vuz == 0) x vuz
gcd0Gcd'2 vvx vvy = gcd0Gcd'0 vvx vvy

gcd0Gcd' x vuz = gcd0Gcd'2 x vuz
gcd0Gcd' x y = gcd0Gcd'0 x y

The bindings of the following Let/Where expression
(fromIntegral q,r :% y)
where 
q  = q1 vu30
q1 (q,zu) = q
r  = r1 vu30
r1 (zv,r) = r
vu30  = quotRem x y

are unpacked to the following functions on top level
properFractionQ vyu vyv = properFractionQ1 vyu vyv (properFractionVu30 vyu vyv)

properFractionR vyu vyv = properFractionR1 vyu vyv (properFractionVu30 vyu vyv)

properFractionR1 vyu vyv (zv,r) = r

properFractionQ1 vyu vyv (q,zu) = q

properFractionVu30 vyu vyv = quotRem vyu vyv



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
HASKELL
                          ↳ NumRed

mainModule Main
  ((floor :: RealFrac a => a  ->  Int) :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
HASKELL
                              ↳ Narrow

mainModule Main
  (floor :: RealFrac a => a  ->  Int)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vyw101000)) → new_primMulNat(vyw101000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs(Succ(vyw190000), Succ(vyw300000), vyw31) → new_esEs(vyw190000, vyw300000, vyw31)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNatS(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS(vyw1740, vyw1750)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ DependencyGraphProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Zero) → new_primModNatS(new_primMinusNatS2(vyw174, vyw175), Succ(vyw175))
new_primModNatS00(vyw174, vyw175) → new_primModNatS(new_primMinusNatS2(vyw174, vyw175), Succ(vyw175))
new_primModNatS(Succ(Zero), Zero) → new_primModNatS(new_primMinusNatS1, Zero)
new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primModNatS(Succ(Succ(vyw30000)), Zero) → new_primModNatS(new_primMinusNatS0(vyw30000), Zero)
new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Succ(vyw1770)) → new_primModNatS0(vyw174, vyw175, vyw1760, vyw1770)
new_primModNatS0(vyw174, vyw175, Zero, Zero) → new_primModNatS00(vyw174, vyw175)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS1Zero
new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS0(vyw30000) → Succ(vyw30000)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
QDP
                                          ↳ UsableRulesProof
                                        ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS(Succ(Succ(vyw30000)), Zero) → new_primModNatS(new_primMinusNatS0(vyw30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS1Zero
new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS0(vyw30000) → Succ(vyw30000)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                          ↳ UsableRulesProof
QDP
                                              ↳ QReductionProof
                                        ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS(Succ(Succ(vyw30000)), Zero) → new_primModNatS(new_primMinusNatS0(vyw30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS1
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
QDP
                                                  ↳ RuleRemovalProof
                                        ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS(Succ(Succ(vyw30000)), Zero) → new_primModNatS(new_primMinusNatS0(vyw30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_primModNatS(Succ(Succ(vyw30000)), Zero) → new_primModNatS(new_primMinusNatS0(vyw30000), Zero)

Strictly oriented rules of the TRS R:

new_primMinusNatS0(vyw30000) → Succ(vyw30000)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + 2·x1   
POL(Zero) = 0   
POL(new_primMinusNatS0(x1)) = 2 + 2·x1   
POL(new_primModNatS(x1, x2)) = x1 + x2   



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ RuleRemovalProof
QDP
                                                      ↳ PisEmptyProof
                                        ↳ QDP
                                  ↳ QDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
QDP
                                          ↳ UsableRulesProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Zero) → new_primModNatS(new_primMinusNatS2(vyw174, vyw175), Succ(vyw175))
new_primModNatS00(vyw174, vyw175) → new_primModNatS(new_primMinusNatS2(vyw174, vyw175), Succ(vyw175))
new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Succ(vyw1770)) → new_primModNatS0(vyw174, vyw175, vyw1760, vyw1770)
new_primModNatS0(vyw174, vyw175, Zero, Zero) → new_primModNatS00(vyw174, vyw175)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS1Zero
new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS0(vyw30000) → Succ(vyw30000)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
QDP
                                              ↳ QReductionProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Zero) → new_primModNatS(new_primMinusNatS2(vyw174, vyw175), Succ(vyw175))
new_primModNatS00(vyw174, vyw175) → new_primModNatS(new_primMinusNatS2(vyw174, vyw175), Succ(vyw175))
new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Succ(vyw1770)) → new_primModNatS0(vyw174, vyw175, vyw1760, vyw1770)
new_primModNatS0(vyw174, vyw175, Zero, Zero) → new_primModNatS00(vyw174, vyw175)

The TRS R consists of the following rules:

new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(x0)
new_primMinusNatS1



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
QDP
                                                  ↳ Rewriting
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Zero) → new_primModNatS(new_primMinusNatS2(vyw174, vyw175), Succ(vyw175))
new_primModNatS00(vyw174, vyw175) → new_primModNatS(new_primMinusNatS2(vyw174, vyw175), Succ(vyw175))
new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primModNatS0(vyw174, vyw175, Zero, Zero) → new_primModNatS00(vyw174, vyw175)
new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Succ(vyw1770)) → new_primModNatS0(vyw174, vyw175, vyw1760, vyw1770)

The TRS R consists of the following rules:

new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Zero) → new_primModNatS(new_primMinusNatS2(vyw174, vyw175), Succ(vyw175)) at position [0] we obtained the following new rules:

new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Zero) → new_primModNatS(new_primMinusNatS3(vyw174, vyw175), Succ(vyw175))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
QDP
                                                      ↳ Rewriting
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS00(vyw174, vyw175) → new_primModNatS(new_primMinusNatS2(vyw174, vyw175), Succ(vyw175))
new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Zero) → new_primModNatS(new_primMinusNatS3(vyw174, vyw175), Succ(vyw175))
new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Succ(vyw1770)) → new_primModNatS0(vyw174, vyw175, vyw1760, vyw1770)
new_primModNatS0(vyw174, vyw175, Zero, Zero) → new_primModNatS00(vyw174, vyw175)

The TRS R consists of the following rules:

new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primModNatS00(vyw174, vyw175) → new_primModNatS(new_primMinusNatS2(vyw174, vyw175), Succ(vyw175)) at position [0] we obtained the following new rules:

new_primModNatS00(vyw174, vyw175) → new_primModNatS(new_primMinusNatS3(vyw174, vyw175), Succ(vyw175))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
QDP
                                                          ↳ UsableRulesProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Zero) → new_primModNatS(new_primMinusNatS3(vyw174, vyw175), Succ(vyw175))
new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primModNatS00(vyw174, vyw175) → new_primModNatS(new_primMinusNatS3(vyw174, vyw175), Succ(vyw175))
new_primModNatS0(vyw174, vyw175, Zero, Zero) → new_primModNatS00(vyw174, vyw175)
new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Succ(vyw1770)) → new_primModNatS0(vyw174, vyw175, vyw1760, vyw1770)

The TRS R consists of the following rules:

new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
QDP
                                                              ↳ QReductionProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Zero) → new_primModNatS(new_primMinusNatS3(vyw174, vyw175), Succ(vyw175))
new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primModNatS00(vyw174, vyw175) → new_primModNatS(new_primMinusNatS3(vyw174, vyw175), Succ(vyw175))
new_primModNatS0(vyw174, vyw175, Zero, Zero) → new_primModNatS00(vyw174, vyw175)
new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Succ(vyw1770)) → new_primModNatS0(vyw174, vyw175, vyw1760, vyw1770)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2(x0, x1)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
QDP
                                                                  ↳ QDPOrderProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Zero) → new_primModNatS(new_primMinusNatS3(vyw174, vyw175), Succ(vyw175))
new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primModNatS00(vyw174, vyw175) → new_primModNatS(new_primMinusNatS3(vyw174, vyw175), Succ(vyw175))
new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Succ(vyw1770)) → new_primModNatS0(vyw174, vyw175, vyw1760, vyw1770)
new_primModNatS0(vyw174, vyw175, Zero, Zero) → new_primModNatS00(vyw174, vyw175)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_primModNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primModNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
The remaining pairs can at least be oriented weakly.

new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Zero) → new_primModNatS(new_primMinusNatS3(vyw174, vyw175), Succ(vyw175))
new_primModNatS00(vyw174, vyw175) → new_primModNatS(new_primMinusNatS3(vyw174, vyw175), Succ(vyw175))
new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Succ(vyw1770)) → new_primModNatS0(vyw174, vyw175, vyw1760, vyw1770)
new_primModNatS0(vyw174, vyw175, Zero, Zero) → new_primModNatS00(vyw174, vyw175)
Used ordering: Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + x1   
POL(Zero) = 0   
POL(new_primMinusNatS3(x1, x2)) = x1   
POL(new_primModNatS(x1, x2)) = x1   
POL(new_primModNatS0(x1, x2, x3, x4)) = x1   
POL(new_primModNatS00(x1, x2)) = x1   

The following usable rules [17] were oriented:

new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
                                                                ↳ QDP
                                                                  ↳ QDPOrderProof
QDP
                                                                      ↳ DependencyGraphProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Zero) → new_primModNatS(new_primMinusNatS3(vyw174, vyw175), Succ(vyw175))
new_primModNatS00(vyw174, vyw175) → new_primModNatS(new_primMinusNatS3(vyw174, vyw175), Succ(vyw175))
new_primModNatS0(vyw174, vyw175, Zero, Zero) → new_primModNatS00(vyw174, vyw175)
new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Succ(vyw1770)) → new_primModNatS0(vyw174, vyw175, vyw1760, vyw1770)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
                                                                ↳ QDP
                                                                  ↳ QDPOrderProof
                                                                    ↳ QDP
                                                                      ↳ DependencyGraphProof
QDP
                                                                          ↳ UsableRulesProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Succ(vyw1770)) → new_primModNatS0(vyw174, vyw175, vyw1760, vyw1770)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
                                                                ↳ QDP
                                                                  ↳ QDPOrderProof
                                                                    ↳ QDP
                                                                      ↳ DependencyGraphProof
                                                                        ↳ QDP
                                                                          ↳ UsableRulesProof
QDP
                                                                              ↳ QReductionProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Succ(vyw1770)) → new_primModNatS0(vyw174, vyw175, vyw1760, vyw1770)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
                                                                ↳ QDP
                                                                  ↳ QDPOrderProof
                                                                    ↳ QDP
                                                                      ↳ DependencyGraphProof
                                                                        ↳ QDP
                                                                          ↳ UsableRulesProof
                                                                            ↳ QDP
                                                                              ↳ QReductionProof
QDP
                                                                                  ↳ QDPSizeChangeProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primModNatS0(vyw174, vyw175, Succ(vyw1760), Succ(vyw1770)) → new_primModNatS0(vyw174, vyw175, vyw1760, vyw1770)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw169, vyw170, Zero, Zero) → new_primDivNatS00(vyw169, vyw170)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Succ(vyw1720)) → new_primDivNatS0(vyw169, vyw170, vyw1710, vyw1720)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Zero) → new_primDivNatS(new_primMinusNatS2(vyw169, vyw170), Succ(vyw170))
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS00(vyw169, vyw170) → new_primDivNatS(new_primMinusNatS2(vyw169, vyw170), Succ(vyw170))
new_primDivNatS(Succ(Succ(vyw30000)), Zero) → new_primDivNatS(new_primMinusNatS0(vyw30000), Zero)
new_primDivNatS(Succ(Zero), Zero) → new_primDivNatS(new_primMinusNatS1, Zero)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS1Zero
new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS0(vyw30000) → Succ(vyw30000)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
QDP
                                          ↳ UsableRulesProof
                                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vyw30000)), Zero) → new_primDivNatS(new_primMinusNatS0(vyw30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS1Zero
new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS0(vyw30000) → Succ(vyw30000)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                          ↳ UsableRulesProof
QDP
                                              ↳ QReductionProof
                                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vyw30000)), Zero) → new_primDivNatS(new_primMinusNatS0(vyw30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS1
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
QDP
                                                  ↳ RuleRemovalProof
                                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vyw30000)), Zero) → new_primDivNatS(new_primMinusNatS0(vyw30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(vyw30000) → Succ(vyw30000)

The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_primDivNatS(Succ(Succ(vyw30000)), Zero) → new_primDivNatS(new_primMinusNatS0(vyw30000), Zero)

Strictly oriented rules of the TRS R:

new_primMinusNatS0(vyw30000) → Succ(vyw30000)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + 2·x1   
POL(Zero) = 0   
POL(new_primDivNatS(x1, x2)) = x1 + x2   
POL(new_primMinusNatS0(x1)) = 2 + 2·x1   



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ RuleRemovalProof
QDP
                                                      ↳ PisEmptyProof
                                        ↳ QDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(x0)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
QDP
                                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw169, vyw170, Zero, Zero) → new_primDivNatS00(vyw169, vyw170)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Succ(vyw1720)) → new_primDivNatS0(vyw169, vyw170, vyw1710, vyw1720)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Zero) → new_primDivNatS(new_primMinusNatS2(vyw169, vyw170), Succ(vyw170))
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS00(vyw169, vyw170) → new_primDivNatS(new_primMinusNatS2(vyw169, vyw170), Succ(vyw170))

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS1Zero
new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS0(vyw30000) → Succ(vyw30000)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
QDP
                                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw169, vyw170, Zero, Zero) → new_primDivNatS00(vyw169, vyw170)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Succ(vyw1720)) → new_primDivNatS0(vyw169, vyw170, vyw1710, vyw1720)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Zero) → new_primDivNatS(new_primMinusNatS2(vyw169, vyw170), Succ(vyw170))
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS00(vyw169, vyw170) → new_primDivNatS(new_primMinusNatS2(vyw169, vyw170), Succ(vyw170))

The TRS R consists of the following rules:

new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS0(x0)
new_primMinusNatS1
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(x0)
new_primMinusNatS1



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
QDP
                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw169, vyw170, Zero, Zero) → new_primDivNatS00(vyw169, vyw170)
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Zero) → new_primDivNatS(new_primMinusNatS2(vyw169, vyw170), Succ(vyw170))
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Succ(vyw1720)) → new_primDivNatS0(vyw169, vyw170, vyw1710, vyw1720)
new_primDivNatS00(vyw169, vyw170) → new_primDivNatS(new_primMinusNatS2(vyw169, vyw170), Succ(vyw170))

The TRS R consists of the following rules:

new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Zero) → new_primDivNatS(new_primMinusNatS2(vyw169, vyw170), Succ(vyw170)) at position [0] we obtained the following new rules:

new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Zero) → new_primDivNatS(new_primMinusNatS3(vyw169, vyw170), Succ(vyw170))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
QDP
                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw169, vyw170, Zero, Zero) → new_primDivNatS00(vyw169, vyw170)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Succ(vyw1720)) → new_primDivNatS0(vyw169, vyw170, vyw1710, vyw1720)
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS00(vyw169, vyw170) → new_primDivNatS(new_primMinusNatS2(vyw169, vyw170), Succ(vyw170))
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Zero) → new_primDivNatS(new_primMinusNatS3(vyw169, vyw170), Succ(vyw170))

The TRS R consists of the following rules:

new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primDivNatS00(vyw169, vyw170) → new_primDivNatS(new_primMinusNatS2(vyw169, vyw170), Succ(vyw170)) at position [0] we obtained the following new rules:

new_primDivNatS00(vyw169, vyw170) → new_primDivNatS(new_primMinusNatS3(vyw169, vyw170), Succ(vyw170))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
QDP
                                                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw169, vyw170, Zero, Zero) → new_primDivNatS00(vyw169, vyw170)
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Succ(vyw1720)) → new_primDivNatS0(vyw169, vyw170, vyw1710, vyw1720)
new_primDivNatS00(vyw169, vyw170) → new_primDivNatS(new_primMinusNatS3(vyw169, vyw170), Succ(vyw170))
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Zero) → new_primDivNatS(new_primMinusNatS3(vyw169, vyw170), Succ(vyw170))

The TRS R consists of the following rules:

new_primMinusNatS2(vyw174, vyw175) → new_primMinusNatS3(vyw174, vyw175)
new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
QDP
                                                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw169, vyw170, Zero, Zero) → new_primDivNatS00(vyw169, vyw170)
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Succ(vyw1720)) → new_primDivNatS0(vyw169, vyw170, vyw1710, vyw1720)
new_primDivNatS00(vyw169, vyw170) → new_primDivNatS(new_primMinusNatS3(vyw169, vyw170), Succ(vyw170))
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Zero) → new_primDivNatS(new_primMinusNatS3(vyw169, vyw170), Succ(vyw170))

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS2(x0, x1)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2(x0, x1)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
QDP
                                                                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw169, vyw170, Zero, Zero) → new_primDivNatS00(vyw169, vyw170)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Succ(vyw1720)) → new_primDivNatS0(vyw169, vyw170, vyw1710, vyw1720)
new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Zero) → new_primDivNatS(new_primMinusNatS3(vyw169, vyw170), Succ(vyw170))
new_primDivNatS00(vyw169, vyw170) → new_primDivNatS(new_primMinusNatS3(vyw169, vyw170), Succ(vyw170))

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_primDivNatS(Succ(Succ(vyw30000)), Succ(vyw31000)) → new_primDivNatS0(vyw30000, vyw31000, vyw30000, vyw31000)
The remaining pairs can at least be oriented weakly.

new_primDivNatS0(vyw169, vyw170, Zero, Zero) → new_primDivNatS00(vyw169, vyw170)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Succ(vyw1720)) → new_primDivNatS0(vyw169, vyw170, vyw1710, vyw1720)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Zero) → new_primDivNatS(new_primMinusNatS3(vyw169, vyw170), Succ(vyw170))
new_primDivNatS00(vyw169, vyw170) → new_primDivNatS(new_primMinusNatS3(vyw169, vyw170), Succ(vyw170))
Used ordering: Polynomial interpretation [25]:

POL(Succ(x1)) = 1 + x1   
POL(Zero) = 0   
POL(new_primDivNatS(x1, x2)) = x1   
POL(new_primDivNatS0(x1, x2, x3, x4)) = x1   
POL(new_primDivNatS00(x1, x2)) = x1   
POL(new_primMinusNatS3(x1, x2)) = x1   

The following usable rules [17] were oriented:

new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)
new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Zero, Zero) → Zero



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
                                                                ↳ QDP
                                                                  ↳ QDPOrderProof
QDP
                                                                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw169, vyw170, Zero, Zero) → new_primDivNatS00(vyw169, vyw170)
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Succ(vyw1720)) → new_primDivNatS0(vyw169, vyw170, vyw1710, vyw1720)
new_primDivNatS00(vyw169, vyw170) → new_primDivNatS(new_primMinusNatS3(vyw169, vyw170), Succ(vyw170))
new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Zero) → new_primDivNatS(new_primMinusNatS3(vyw169, vyw170), Succ(vyw170))

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
                                                                ↳ QDP
                                                                  ↳ QDPOrderProof
                                                                    ↳ QDP
                                                                      ↳ DependencyGraphProof
QDP
                                                                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Succ(vyw1720)) → new_primDivNatS0(vyw169, vyw170, vyw1710, vyw1720)

The TRS R consists of the following rules:

new_primMinusNatS3(Zero, Succ(vyw1750)) → Zero
new_primMinusNatS3(Succ(vyw1740), Succ(vyw1750)) → new_primMinusNatS3(vyw1740, vyw1750)
new_primMinusNatS3(Zero, Zero) → Zero
new_primMinusNatS3(Succ(vyw1740), Zero) → Succ(vyw1740)

The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
                                                                ↳ QDP
                                                                  ↳ QDPOrderProof
                                                                    ↳ QDP
                                                                      ↳ DependencyGraphProof
                                                                        ↳ QDP
                                                                          ↳ UsableRulesProof
QDP
                                                                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Succ(vyw1720)) → new_primDivNatS0(vyw169, vyw170, vyw1710, vyw1720)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS3(Zero, Zero)
new_primMinusNatS3(Zero, Succ(x0))
new_primMinusNatS3(Succ(x0), Zero)
new_primMinusNatS3(Succ(x0), Succ(x1))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                    ↳ DependencyGraphProof
                                      ↳ AND
                                        ↳ QDP
                                        ↳ QDP
                                          ↳ UsableRulesProof
                                            ↳ QDP
                                              ↳ QReductionProof
                                                ↳ QDP
                                                  ↳ Rewriting
                                                    ↳ QDP
                                                      ↳ Rewriting
                                                        ↳ QDP
                                                          ↳ UsableRulesProof
                                                            ↳ QDP
                                                              ↳ QReductionProof
                                                                ↳ QDP
                                                                  ↳ QDPOrderProof
                                                                    ↳ QDP
                                                                      ↳ DependencyGraphProof
                                                                        ↳ QDP
                                                                          ↳ UsableRulesProof
                                                                            ↳ QDP
                                                                              ↳ QReductionProof
QDP
                                                                                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vyw169, vyw170, Succ(vyw1710), Succ(vyw1720)) → new_primDivNatS0(vyw169, vyw170, vyw1710, vyw1720)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: